Runtime Complexity (innermost) proof of /tmp/tmp698o3H/thetrickSize.xml

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

0 CpxRelTRS

↳1 RelTrsToTrsProof (UPPER BOUND(ID), 0 ms)

↳2 CpxTRS

↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 9 ms)

↳4 CdtProblem

↳5 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳6 CdtProblem

↳7 CdtUsableRulesProof (⇔, 0 ms)

↳8 CdtProblem

↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 175 ms)

↳10 CdtProblem

↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 25 ms)

↳12 CdtProblem

↳13 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 42 ms)

↳16 CdtProblem

↳17 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 33 ms)

↳20 CdtProblem

↳21 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳22 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

lt0(Nil, Cons(x', xs)) → True
lt0(Cons(x', xs'), Cons(x, xs)) → lt0(xs', xs)
g(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lt0(x, Nil) → False
g(x, Cons(x', xs)) → g[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
f(x, Cons(x', xs)) → f[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
number4(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(x, y) → Cons(f(x, y), Cons(g(x, y), Nil))

The (relative) TRS S consists of the following rules:

g[Ite][False][Ite](False, Cons(x, xs), y) → g(xs, Cons(Cons(Nil, Nil), y))
g[Ite][False][Ite](True, x', Cons(x, xs)) → g(x', xs)
f[Ite][False][Ite](False, Cons(x, xs), y) → f(xs, Cons(Cons(Nil, Nil), y))
f[Ite][False][Ite](True, x', Cons(x, xs)) → f(x', xs)

Rewrite Strategy: INNERMOST

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

transformed relative TRS to TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

The TRS R consists of the following rules:

lt0(Nil, Cons(x', xs)) → True
lt0(Cons(x', xs'), Cons(x, xs)) → lt0(xs', xs)
g(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(x, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
lt0(x, Nil) → False
g(x, Cons(x', xs)) → g[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
f(x, Cons(x', xs)) → f[Ite][False][Ite](lt0(x, Cons(Nil, Nil)), x, Cons(x', xs))
number4(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(x, y) → Cons(f(x, y), Cons(g(x, y), Nil))
g[Ite][False][Ite](False, Cons(x, xs), y) → g(xs, Cons(Cons(Nil, Nil), y))
g[Ite][False][Ite](True, x', Cons(x, xs)) → g(x', xs)
f[Ite][False][Ite](False, Cons(x, xs), y) → f(xs, Cons(Cons(Nil, Nil), y))
f[Ite][False][Ite](True, x', Cons(x, xs)) → f(x', xs)

Rewrite Strategy: INNERMOST

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)

Tuples:

LT0(Nil, Cons(z0, z1)) → c
LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
LT0(z0, Nil) → c2
G(z0, Nil) → c3
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c5
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
NOTEMPTY(Cons(z0, z1)) → c7
NOTEMPTY(Nil) → c8
NUMBER4(z0) → c9
GOAL(z0, z1) → c10(F(z0, z1), G(z0, z1))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Nil, Cons(z0, z1)) → c
LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
LT0(z0, Nil) → c2
G(z0, Nil) → c3
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Nil) → c5
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
NOTEMPTY(Cons(z0, z1)) → c7
NOTEMPTY(Nil) → c8
NUMBER4(z0) → c9
GOAL(z0, z1) → c10(F(z0, z1), G(z0, z1))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:none
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

LT0, G, F, NOTEMPTY, NUMBER4, GOAL, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

GOAL(z0, z1) → c10(F(z0, z1), G(z0, z1))

Removed 7 trailing nodes:

NOTEMPTY(Cons(z0, z1)) → c7
NUMBER4(z0) → c9
NOTEMPTY(Nil) → c8
LT0(Nil, Cons(z0, z1)) → c
F(z0, Nil) → c5
LT0(z0, Nil) → c2
G(z0, Nil) → c3

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False
g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:none
Defined Rule Symbols:

lt0, g, f, notEmpty, number4, goal, g[Ite][False][Ite], f[Ite][False][Ite]

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(7) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

g(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
g(z0, Cons(z1, z2)) → g[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
f(z0, Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
f(z0, Cons(z1, z2)) → f[Ite][False][Ite](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2))
notEmpty(Cons(z0, z1)) → True
notEmpty(Nil) → False
number4(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))
goal(z0, z1) → Cons(f(z0, z1), Cons(g(z0, z1), Nil))
g[Ite][False][Ite](False, Cons(z0, z1), z2) → g(z1, Cons(Cons(Nil, Nil), z2))
g[Ite][False][Ite](True, z0, Cons(z1, z2)) → g(z0, z2)
f[Ite][False][Ite](False, Cons(z0, z1), z2) → f(z1, Cons(Cons(Nil, Nil), z2))
f[Ite][False][Ite](True, z0, Cons(z1, z2)) → f(z0, z2)

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:none
Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))

We considered the (Usable) Rules:none
And the Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x₁, x₂)) = [1] + x₂
POL(F(x₁, x₂)) = x₁
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = x₂
POL(False) = 0
POL(G(x₁, x₂)) = 0
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(LT0(x₁, x₂)) = 0
POL(Nil) = 0
POL(True) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(lt0(x₁, x₂)) = 0

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

We considered the (Usable) Rules:none
And the Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x₁, x₂)) = [2] + x₂
POL(F(x₁, x₂)) = 0
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(False) = 0
POL(G(x₁, x₂)) = [3] + [2]x₁ + x₂
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = [1] + [2]x₂ + x₃
POL(LT0(x₁, x₂)) = 0
POL(Nil) = 0
POL(True) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(lt0(x₁, x₂)) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

We considered the (Usable) Rules:none
And the Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x₁, x₂)) = [2] + x₂
POL(F(x₁, x₂)) = [2]x₁ + [2]x₂
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [2]x₂ + [2]x₃
POL(False) = 0
POL(G(x₁, x₂)) = 0
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = 0
POL(LT0(x₁, x₂)) = 0
POL(Nil) = 0
POL(True) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(lt0(x₁, x₂)) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))

K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))

We considered the (Usable) Rules:none
And the Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(Cons(x₁, x₂)) = [1] + x₂
POL(F(x₁, x₂)) = [1] + [3]x₁ + x₂
POL(F[ITE][FALSE][ITE](x₁, x₂, x₃)) = [3]x₂ + x₃
POL(False) = 0
POL(G(x₁, x₂)) = [2] + [3]x₁ + [2]x₂
POL(G[ITE][FALSE][ITE](x₁, x₂, x₃)) = [1] + [3]x₂ + [2]x₃
POL(LT0(x₁, x₂)) = x₂
POL(Nil) = 0
POL(True) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c13(x₁)) = x₁
POL(c14(x₁)) = x₁
POL(c4(x₁, x₂)) = x₁ + x₂
POL(c6(x₁, x₂)) = x₁ + x₂
POL(lt0(x₁, x₂)) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

lt0(Nil, Cons(z0, z1)) → True
lt0(Cons(z0, z1), Cons(z2, z3)) → lt0(z1, z3)
lt0(z0, Nil) → False

Tuples:

LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))

S tuples:none
K tuples:

F[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c13(F(z1, Cons(Cons(Nil, Nil), z2)))
G(z0, Cons(z1, z2)) → c4(G[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
G[ITE][FALSE][ITE](False, Cons(z0, z1), z2) → c11(G(z1, Cons(Cons(Nil, Nil), z2)))
G[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c12(G(z0, z2))
F[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) → c14(F(z0, z2))
F(z0, Cons(z1, z2)) → c6(F[ITE][FALSE][ITE](lt0(z0, Cons(Nil, Nil)), z0, Cons(z1, z2)), LT0(z0, Cons(Nil, Nil)))
LT0(Cons(z0, z1), Cons(z2, z3)) → c1(LT0(z1, z3))

Defined Rule Symbols:

lt0

Defined Pair Symbols:

LT0, G, F, G[ITE][FALSE][ITE], F[ITE][FALSE][ITE]

Compound Symbols:

c1, c4, c6, c11, c12, c13, c14

(21) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) RelTrsToTrsProof (UPPER BOUND(ID) transformation)

(2) Obligation:

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(6) Obligation:

(7) CdtUsableRulesProof (EQUIVALENT transformation)

(8) Obligation:

(9) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(10) Obligation:

(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(12) Obligation:

(13) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

(17) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(18) Obligation:

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(20) Obligation:

(21) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(22) BOUNDS(1, 1)